YES 4.844 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule Main
  ((rangeSize :: (Ordering,Ordering ->  Int) :: (Ordering,Ordering ->  Int)

module Main where
  import qualified Prelude



Lambda Reductions:
The following Lambda expression
\z→if y >= z && z >= x then z : [] else []

is transformed to
range0 y x z = if y >= z && z >= x then z : [] else []

The following Lambda expression
\s→if y > s then 1 else 0

is transformed to
index0 y s = if y > s then 1 else 0



↳ HASKELL
  ↳ LR
HASKELL
      ↳ IFR

mainModule Main
  ((rangeSize :: (Ordering,Ordering ->  Int) :: (Ordering,Ordering ->  Int)

module Main where
  import qualified Prelude



If Reductions:
The following If expression
if y > s then 1 else 0

is transformed to
index00 True = 1
index00 False = 0

The following If expression
if y >= z && z >= x then z : [] else []

is transformed to
range00 z True = z : []
range00 z False = []

The following If expression
if y >= z && z >= x then sum (map (index0 y) (range (x,y))) else error []

is transformed to
index1 y x True = sum (map (index0 y) (range (x,y)))
index1 y x False = error []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
HASKELL
          ↳ BR

mainModule Main
  ((rangeSize :: (Ordering,Ordering ->  Int) :: (Ordering,Ordering ->  Int)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
r@(vv,vw)

is replaced by the following term
(vv,vw)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
HASKELL
              ↳ COR

mainModule Main
  ((rangeSize :: (Ordering,Ordering ->  Int) :: (Ordering,Ordering ->  Int)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
compare x y
 | x == y
 = EQ
 | x <= y
 = LT
 | otherwise
 = GT

is transformed to
compare x y = compare3 x y

compare0 x y True = GT

compare2 x y True = EQ
compare2 x y False = compare1 x y (x <= y)

compare1 x y True = LT
compare1 x y False = compare0 x y otherwise

compare3 x y = compare2 x y (x == y)

The following Function with conditions
rangeSize (vv,vw)
 | null (range (vv,vw))
 = 0
 | otherwise
 = index (vv,vwvw + 1

is transformed to
rangeSize (vv,vw) = rangeSize2 (vv,vw)

rangeSize1 vv vw True = 0
rangeSize1 vv vw False = rangeSize0 vv vw otherwise

rangeSize0 vv vw True = index (vv,vwvw + 1

rangeSize2 (vv,vw) = rangeSize1 vv vw (null (range (vv,vw)))

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
HASKELL
                  ↳ NumRed

mainModule Main
  ((rangeSize :: (Ordering,Ordering ->  Int) :: (Ordering,Ordering ->  Int)

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ NumRed
HASKELL
                      ↳ Narrow

mainModule Main
  (rangeSize :: (Ordering,Ordering ->  Int)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ NumRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(ww160), Succ(ww900)) → new_primMinusNat(ww160, ww900)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ NumRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
QDP
                            ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(ww160), Succ(ww900)) → new_primPlusNat(ww160, ww900)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: